$\forall$${\it the\_es}$:event\_system\{i:l\}, $j$:es{-}E(${\it the\_es}$).
\\[0ex]($\neg$($\uparrow$es{-}first(${\it the\_es}$; $j$))) $\Rightarrow$ es{-}locl(${\it the\_es}$; es{-}pred(${\it the\_es}$; $j$); $j$)